mk_igrp(T;op;id;inv) == <T, x,y. tt, x,y. tt, op, id, inv> 

latex

Up	groups 1
Wellformedness Lemmas	mk igrp wf
Definitions	tt